COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	proof? 
C00008 00003
C00010 00004	Representation in AI.
C00013 00005	Solutions.
C00014 ENDMK
C⊗;
proof? 
* APE started.
* 
* 
* 
* 
* 
* 
* 7. IN(UNDER_BANANAS,ROOM)
   deps: NIL

* 8. IN(CORNER,ROOM)
   deps: NIL

* 9. AT(BOX,CORNER,S0)
   deps: NIL

* 10. AT(MONKEY,CORNER,S0)
    deps: NIL

* 11. ∀X Y Z S.IN(X,ROOM)∧IN(Y,ROOM)∧AT(Z,X,S)∧AT(MONKEY,X,S)⊃
              AT(Z,Y,RESULT(DOES(MONKEY,MOVE(Z,Y)),S))∧
              AT(MONKEY,Y,RESULT(DOES(MONKEY,MOVE(Z,Y)),S))
    deps: NIL

* 12. ∀S X.AT(BOX,X,S)∧AT(MONKEY,X,S)⊃
          AT(MONKEY,TOP(BOX),RESULT(DOES(MONKEY,CLIMB(BOX)),S))
    deps: NIL

* 13. ∀S.AT(MONKEY,TOP(BOX),S)∧AT(BOX,UNDER_BANANAS,S)⊃CAN_GET(MONKEY,BANANAS,S)
    deps: NIL

* 14. ∀S X.AT(BOX,X,S)∧AT(MONKEY,X,S)⊃
          AT(MONKEY,TOP(BOX),RESULT(DOES(MONKEY,CLIMB(BOX)),S))∧
          AT(BOX,X,RESULT(DOES(MONKEY,CLIMB(BOX)),S))
    deps: NIL

* 15. AT(BOX,UNDER_BANANAS,RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0))∧
    AT(MONKEY,UNDER_BANANAS,RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0))
    deps: NIL

* 16. AT(MONKEY,TOP(BOX),
       RESULT(DOES(MONKEY,CLIMB(BOX)),
              RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))
    deps: NIL

* 17. AT(BOX,UNDER_BANANAS,
       RESULT(DOES(MONKEY,CLIMB(BOX)),
              RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))⊃
     CAN_GET(MONKEY,BANANAS,
             RESULT(DOES(MONKEY,CLIMB(BOX)),
                    RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))
    deps: NIL

* 18. AT(MONKEY,TOP(BOX),
       RESULT(DOES(MONKEY,CLIMB(BOX)),
              RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))∧
    AT(BOX,UNDER_BANANAS,
       RESULT(DOES(MONKEY,CLIMB(BOX)),
              RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))
    deps: NIL

* 19. CAN_GET(MONKEY,BANANAS,
            RESULT(DOES(MONKEY,CLIMB(BOX)),
                   RESULT(DOES(MONKEY,MOVE(BOX,UNDER_BANANAS)),S0)))
    deps: NIL

* .....done.
* 
(pretty-proof ape ape)
;;;
(wipe-out)
(proof ape)
(decl (under_bananas room corner box s0 monkey bananas) ground constant)
(decl (x y z s) ground) 
(decl in |ground⊗ground → truthval| constant)
(decl (does move result) |ground⊗ground → ground| constant)
(decl (can_get at) |ground⊗ground⊗ground → truthval| constant)
(decl (climb top) |ground → ground| constant)

(axiom |in(under_bananas, room)|)
(axiom |in(corner, room)|)
(axiom |at(box,corner,s0)|)
(axiom |at(monkey,corner,s0)|)

(axiom |∀x y z s.in(x,room)∧in(y,room) ∧ at(z,x,s) ∧ at(monkey,x,s)
     ⊃ at(z,y,result(does(monkey, move(z,y)),s))
     ∧ at(monkey,y,result(does(monkey, move(z,y)),s))|)

(axiom |∀s x.at(box,x,s) ∧ at(monkey,x,s)
     ⊃  at(monkey,top(box),result(does(monkey,climb(box)),s))|)

(axiom |∀s.at(monkey,top(box),s) ∧ at(box,under_bananas,s)
     ⊃ can_get(monkey,bananas,s)|)

(axiom |∀s x.at(box,x,s) ∧ at(monkey,x,s)
     ⊃  at(monkey,top(box),result(does(monkey,climb(box)),s))
     ∧  at(box,x,result(does(monkey,climb(box)),s))|)

(∀e ((x.corner)(y.under_bananas)(z.box)(s.s0)) 11 |*7:10*nil|)

(∀e ((x.under_bananas)(s.|result(does(monkey,move(box,under_bananas)),s0)|)) 12
|nil**(7:10+15)*nil|)

(∀e s |result(does(monkey,climb(box)),
                    result(does(monkey,move(box,under_bananas)),s0))|
13 |nil**7:10**16*nil|)

(∀e ((x.under_bananas)(s.|result(does(monkey,move(box,under_bananas)),s0)|)) 14
|nil**(7:10+15)*nil|)

(∀e s |result(does(monkey,climb(box)),
                    result(does(monkey,move(box,under_bananas)),s0))|
13 |nil**7:10**18*nil|)
Representation in AI.

	The following is a set of first order axioms for the
monkey-and-bananas problem.  The variable  s  is used to represent
situations and the constant  s0  is an initial situation.
result(e, s)  is the situation that results when event  e  occurs
in situation  s.  The events that concern us are actions of the
form  does(p, a)  where  p  is a "person" and  a  is an action.
The only person mentioned is  monkey  and the actions he can perform
are moving the box and and climbing it.  The axioms describe the
initial situation and give the effects of performing actions.  The
formula  at(x,y,s)  is used to assert that the person or object  x
is at the place  y  in the situation  s, and the formula  in(x,y)
asserts that the object or person  x  is permanently (as far as this
axiomatization goes) in the place  y.

1. in(under_bananas, room)

2. in(corner, room)

3. at(box,corner,s0)

4. at(monkey,corner,s0)

5. ∀x y z s.in(x,room)∧in(y,room) ∧ at(z,x,s) ∧ at(monkey,x,s)
     ⊃ at(z,y,result(does(monkey, move(z,y)),s))
     ∧ at(monkey,y,result(does(monkey, move(z,y)),s))

6. ∀s x.at(box,x,s) ∧ at(monkey,x,s)
     ⊃  at(monkey,top(box),result(does(monkey,climb(box)),s))

7. ∀s.at(monkey,top(box),s) ∧ at(box,under_bananas,s)
     ⊃ can_get(monkey,bananas,s)

Questions:

1. Why are these axioms inadequate for showing that the monkey can get
the bananas by moving the box under the bananas and climbing the box?

2. What is this difficulty called?

3. Modify one of the axioms in a plausible way so that it can be shown
that the monkey can get the bananas.

4. What is unsatisfactory about such modified sets of axioms.

5. Mention what approaches you know to solving the problem.

Solutions.

1. It doesn't follow that when the monkey climbs the box, the box will
still be under the bananas.

2. This is the "frame problem".

3. Axiom 6 should be replaced by

6'. ∀s x.at(box,x,s) ∧ at(monkey,x,s)
     ⊃  at(monkey,top(box),result(does(monkey,climb(box)),s))
     ∧  at(box,x,result(does(monkey,climb(box)),s))

4. This approach requires that the axiom giving the effect of an event
describe all the predicates that are unmodified by the event.

5. STRIPS, frames, microplanner, and non-monotonic reasoning for example.